$\forall$$A$, $B$:Type\{i\}. es{-}component\{i:l\}($A$; $B$) $\in$ Type\{i'\}